﻿using System;
using System.Diagnostics;
using System.Collections.Generic;

using alib.Debugging;
using alib.Enumerable;

namespace agree
{
	public unsafe sealed partial class Unification : IDisposable
	{
		public const int None = 0;
		public const int FirstSubsumesSecond = 1;
		public const int SecondSubsumesFirst = 2;
		public const int Equivalent = 3;
		public const int Bottom = -4;	// note: doesn't interfere with subsumption bit-testing
		const int FirstNotSubsuming = ~FirstSubsumesSecond;
		const int SecondNotSubsuming = ~SecondSubsumesFirst;

		int subsumption;

		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		/// 
		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		void _subsumption_body(Edge.Flag f, Slot* ps0, Slot* ps1)
		{
			pinfo* pi0 = pbx + ps0->tfsix, pi1 = pbx + ps1->tfsix;
			ushort* pfix = *(ushort**)((long)rgpfix + ((int)f << 3));
			do
			{
				int ix0, ix1;
				if ((ix0 = pi0->_fetch_ix_only(*pfix, ps0->m_src)) == 0)
					subsumption &= SecondNotSubsuming;
				else if ((ix1 = pi1->_fetch_ix_only(*pfix, ps1->m_src)) == 0)
					subsumption &= FirstNotSubsuming;
				else
				{
					Slot* nps0, nps1;
					bool bf0 = _load_node_no_fwd(out nps0, pi0->tfsix, ix0);
					bool bf1 = _load_node_no_fwd(out nps1, pi1->tfsix, ix1);

					if (!bf0 && !bf1)
					{
					}
					else if (!bf0)
					{
						if ((subsumption &= SecondNotSubsuming) <= 0)
							return;
					}
					else if (!bf1)
					{
						if ((subsumption &= FirstNotSubsuming) <= 0)
							return;
					}
					else if (nps0 != nps1)
					{
						subsumption = None;
						return;
					}
					else
					{
					}

					nps0->forward = pi1->uix0 + ix1;

					_duplex_sub(nps0, nps1);
				}
			}
			while (subsumption > 0 && *++pfix != 0xFFFF);
		}

		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		/// <summary>
		/// -4 : tfs0 ⊓ tfs1 = ⊥
		/// 0 : no subsumption relationship (possibly ⊥)
		/// 1 : tfs0 ⊑ tfs1
		/// 2 : tfs1 ⊑ tfs0
		/// 3 : tfs0 == tfs1
		/// </summary>
		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		int _duplex_sub(Slot* ps0, Slot* ps1)
		{
			Edge.Flag f = _subsumption_node(ps0, ps1);

			if (subsumption > 0 && (f & Edge.Flag.EtmNonBareType) != 0)
				_subsumption_body(f, ps0, ps1);

			return subsumption;
		}

		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		/// <summary>
		/// 
		/// </summary>
		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		Edge.Flag _subsumption_node(Slot* ps0, Slot* ps1)
		{
			/// check for a re-entrancy that is present in one TFS but not the other
			Edge.Flag f0 = ps0->f, f1 = ps1->f;

			/// now that the coreference bit is stripped out, check type subsumption
			if (f0 == f1)
				return f0;
			if (f1 == 0)
			{
				subsumption &= FirstNotSubsuming;
				return f0;
			}
			if (f0 == 0)
			{
				subsumption &= SecondNotSubsuming;
				return f1;
			}

			Edge.Flag f;
			if ((f0 & f1) >= Edge.Flag.EtmLeafType ||
				(f = f1 < f0 ? tu.UnifyTypesHiLo(f1, f0) : tu.UnifyTypesHiLo(f0, f1)) < 0)
			{
				subsumption = Bottom;
				return Edge.Flag.Bottom;
			}
			else if (f == f0)
				subsumption &= FirstNotSubsuming;
			else if (f == f1)
				subsumption &= SecondNotSubsuming;
			else
				subsumption = None;
			return f;
		}

		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		/// <summary>
		/// 
		/// </summary>
		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		int _check_subsumption_pairs(IEnumerable<Pairing<TfsSlot>> rgpr)
		{
			this.subsumption = Equivalent;
			var e = rgpr.GetEnumerator();
			if (!e.MoveNext())
				return subsumption;

			Pairing<TfsSlot> pr = e.Current;

			pinfo* pi0 = _init_tfs(pr.x.tfs);
			pinfo* pi1 = _init_tfs(pr.y.tfs);
			do
			{
				pr = e.Current;

				Slot* ps0, ps1;
				_load_node_no_fwd(out ps0, pi0->tfsix, pr.x.ix1);
				_load_node_no_fwd(out ps1, pi1->tfsix, pr.y.ix1);

				_duplex_sub(ps0, ps1);
			}
			while (subsumption > 0 && e.MoveNext());

			return freeU(subsumption);
		}

		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		/// <summary>
		/// 
		/// </summary>
		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		bool subsumes(Slot* ps_sup, Slot* ps_sub)
		{
			this.subsumption = Equivalent;
			int result = _duplex_sub(ps_sup, ps_sub);
			return result == 1 || result == 3;
		}
	};
}